Nuprl Lemma : Rall-cons
11,40
postcript
pdf
u
,
v
,
R
:top. sqequal(Rall(cons(
u
;
v
);
x
.
R
(
x
)); Rplus(
R
(
u
); Rall(
v
;
x
.
R
(
x
))))
latex
Definitions
t
T
,
reduce(
f
;
k
;
as
)
,
Y
,
map(
f
;
as
)
,
Rlist(
L
)
,
Rall(
L
;
x
.
R
(
x
))
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
u,v,R:top. sqequal(Rall(cons(u; v); x.R(x)); Rplus(R(u); Rall(v; x.R(x)))) u,v,R:top. sqequal(Rall(cons(u; v); x.R(x)); Rplus(R(u); Rall(v; x.R(x)))) 
Tx:A. B(x)